es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id} ). e@loc(e'). Dec(P(e))  Dec(ee'.P(e)) 

latex

Definitions	ES, t  T, x:A. B(x), E, , loc(e), Id, x(s), Dec(P), x. t(x), e@i. P(e), P  Q, b, False, A, e<e'. P(e), P & Q, ee'.P(e), P  Q, P  Q, {T}
Lemmas	all functionality wrt iff, implies functionality wrt iff, decidable functionality, alle-le-iff, alle-le wf, decidable and, alle-lt wf, es-loc-pred, decidable alle-lt, alle-at wf, decidable wf, Id wf, es-loc wf, es-E wf, event system wf